Documentation preview for this PR (built with commit 67496ed; changes) is ready! 🎉
This preview will update shortly after each push to this PR.

I'm not entirely sure that my algorithm for computing Taelman's unit is correct. I need to think more about this.

Finally, I prefer to remove things about Taelman's unit here and keep it for another PR.

So again here, it seems the failing doctest is independent from this PR. Could you please merge from develop?

Here is a proof that the algorithm used in this PR is correct.

Let $\varpi = 1/T$; it is a uniformizer of the completion as infinity $K_\infty$.
For each positive integer $n$, let $I_n$ be the set of elements of $K_\infty$ of valuation at least $n$, i.e. $I_n$ is the $\mathbb F_q$-subvector space generated by $\varpi^m$ with $m \geq n$.
Let $s$ be a positive integer such that the $E$-logarithm converges on $I_s$ and induces a bijection on this space.
We notice that $\exp_E(\varpi^{s-1}) \equiv \varpi^{s-1} \pmod {\varpi^s}$.

Consider now $x \in K_\infty$ and decompose it as $x = y + a_{s-1} \varpi^{s-1} + \cdots + a_1 \varpi + z$ with $y \in I_s$ and $z \in A$.
We deduce that
$$\exp_E(x) \equiv a_{s-1} \varpi^{s-1} + a_{s-2} \phi_T(\varpi^{s-1}) + \cdots + a_1 \phi_T^{s-2}(\varpi) \pmod {I_s + A}.$$
Since the action of $E_T$ corresponds to the multiplication by $T$ in $E(K_\infty)$, we obtain the claim of the description of this PR.

In the implementation, we choose a specific value of $s$, which is
$$s = \max_i \Big\lfloor \frac{\deg g_i }{q^i-1} \Big\rfloor$$
where $g_i$ is the $i$-th coefficient of $E_T$. This comes from the fact that $\phi_T(\varpi^n) \equiv \varpi^n \pmod {I_{n-1}}$ for all $n \geq s$. Hence, taking $s$ as above does not change the final result of the computation.

🍸